Nuprl Lemma : last-cons
0,22
postcript
pdf
x
:Top,
as
:Top List. last(
x
.
as
) ~ if null(
as
)
x
else last(
as
) fi
latex
Definitions
hd(
l
)
,
i
<
j
,
i
j
,
l
[
i
]
,
last(
L
)
,
Top
,
t
T
,
x
:
A
.
B
(
x
)
,
i
j
,
P
Q
,
False
,
A
,
A
B
,
P
&
Q
,
i
j
<
k
,
{
i
..
j
}
,
||
as
||
Lemmas
select
cons
tl
sq
,
length
cons
,
non
neg
length
,
length
wf1
,
top
wf
origin
x:Top, as:Top List. last(x.as) ~ if null(as)
x else last(as) fi x:Top, as:Top List. last(x.as) ~ if null(as) x else last(as) fi 
j
j
Tx:A. B(x)
j
Q
AB j < k
}